Fixes for move of univ_constraint to a separated, qualified namespace

theories/L1g/compile.v

@@ -3,7 +3,7 @@ Require Import Coq.Lists.List.
 Require Import Coq.Strings.String.
 Require Import Coq.omega.Omega.
 Require Import Coq.Bool.Bool.
-Require Import Template.Ast.
+Require Import Template.Ast Template.kernel.univ.
 Require Import Common.Common.
 
 Local Open Scope string_scope.
@@ -278,8 +278,8 @@ Function term_Term (t:term) : Term :=
     | tRel n => TRel n
     | tSort srt =>
       TSort (match srt with 
-             | (lProp, false) :: nil => SProp
-             | (lSet, false) :: nil => SSet
+             | (Level.lProp, false) :: nil => SProp
+             | (Level.lSet, false) :: nil => SSet
              | _ => SType  (* throwing away sort info *)
              end)
     | tCast tm _ (tCast _ _ (tSort sProp)) => mkProof (term_Term tm)
@@ -322,7 +322,7 @@ Fixpoint program_Pgm
     | PIn t => {| main:= (term_Term dtEnv t); env:= e |}
     | PConstr nm us ty t p =>
       program_Pgm dtEnv p (cons (pair nm (ecTrm (term_Term dtEnv t))) e)
-    | PType nm npar ibs p =>
+    | PType nm uctx npar ibs p =>
       let Ibs := ibodies_itypPack ibs in
       program_Pgm dtEnv p (cons (pair nm (ecTyp Term npar Ibs)) e)
     | PAxiom nm us _ p =>

theories/common/AstCommon.v

@@ -1,4 +1,4 @@
-
+Require Import Template.kernel.univ.
 Require Export Template.Ast.
 Require Import Template.Template.
 Require Import Coq.Strings.String.
@@ -36,10 +36,10 @@ induction s1; induction s2; try (solve [right; intros h; discriminate]).
   + right. injection. intuition.
 Defined.
 
-Lemma level_dec : forall x y : level, {x = y} + {x <> y}.
+Lemma level_dec : forall x y : Level.t, {x = y} + {x <> y}.
 Proof. decide equality. apply String.string_dec. apply NPeano.Nat.eq_dec. Defined.
 
-Lemma level_bool_dec : forall x y : level * bool, {x = y} + {x <> y}.
+Lemma level_bool_dec : forall x y : Level.t * bool, {x = y} + {x <> y}.
 Proof. intros [l b] [l' b']. decide equality. apply Bool.bool_dec. apply level_dec. Defined.
 
 Lemma universe_dec: forall x y : universe, {x = y} + {x <> y}.
@@ -53,10 +53,11 @@ try (solve [left; reflexivity]).
 Defined.
 
 Lemma inductive_dec: forall (s1 s2:inductive), {s1 = s2}+{s1 <> s2}.
-induction s1; induction s2.
-destruct (string_dec k k0); destruct (eq_nat_dec n n0); subst;
+  intros [mind i] [mind' i'].
+  destruct (string_dec mind mind');
+    destruct (eq_nat_dec i i'); subst;
 try (solve [left; reflexivity]); 
-right; intros h; elim n1; injection h; intuition.
+right; intros h; elim n; injection h; intuition.
 Defined.
 
 Lemma nat_list_dec : forall l1 l2 : list nat, {l1 = l2} + {l1 <> l2}.
@@ -220,7 +221,7 @@ Fixpoint program_datatypeEnv (p:program) (e:environ) : environ :=
   match p with
     | PIn _ => e
     | PConstr _ _ _ _ p => program_datatypeEnv p e
-    | PType nm npar ibs p =>
+    | PType nm uctx npar ibs p =>
       let Ibs := ibodies_itypPack ibs in
       program_datatypeEnv p (cons (pair nm (ecTyp npar Ibs)) e)
     | PAxiom nm _ _ p =>

theories/common/Common.v

@@ -4,5 +4,5 @@ Require Export Template.Ast.
 
 Require Export Common.exceptionMonad.
 Require Export Common.RandyPrelude.
-Require Export Common.classes.
 Require Export Common.AstCommon.
+Require Export Common.classes.