Commit 85faa1d3 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Fix module prefix

parent 30f8c1b5
Add LoadPath "../../" as rt.
Require Import util.Vbase util.lemmas util.divround.
Require Import analysis.basic.bertogna_fp_theory.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.analysis.basic.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
......
Add LoadPath "../../" as rt.
Require Import util.Vbase util.lemmas util.divround.
Require Import analysis.jitter.bertogna_fp_theory.
Require Import rt.util.Vbase util.lemmas rt.util.divround.
Require Import rt.analysis.jitter.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
......
Add LoadPath ".." as rt.
Require Import util.Vbase util.ssromega.
Require Import rt.util.Vbase rt.util.ssromega.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple path div.
(* Here we define a more verbose notation for projections of pairs... *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment