Merge pull request #50 from coq-community/v8.10+no-template-annot

Remove template annotations for 8.10 branch

.travis.yml

@@ -12,7 +12,7 @@ opam: &OPAM
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
       opam update -y
-      opam pin add ${CONTRIB_NAME} . -y --no-action
+      opam pin add ${CONTRIB_NAME} . -y -n -k path
       opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only
       opam config list
       opam repo list

theories/AAC.v

@@ -161,14 +161,14 @@ Module Sym.
 
     Register type_of as aac_tactics.internal.sym.type_of.
     Register rel_of as aac_tactics.internal.sym.rel_of.
-   
+
   (** a symbol package contains an arity,
      a value of the corresponding type,
      and a proof that the value is a proper morphism *)
-  #[universes(template)]
-  Record pack  : Type := mkPack {
+
+  Record pack : Type := mkPack {
     ar : nat;
-    value :> type_of  ar;
+    value :> type_of ar;
     morph : Proper (rel_of ar) value
                            }.
 
@@ -190,7 +190,6 @@ Module Bin.
   Section t.
     Context {X} {R: relation X}.
 
-    #[universes(template)]
     Record pack := mk_pack {
       value:> X -> X -> X;
       compat: Proper (R ==> R ==> R) value;
@@ -226,7 +225,6 @@ Section s.
     uf_desc: Unit R (Bin.value (e_bin uf_idx)) u
   }.
 
-  #[universes(template)]
   Record unit_pack := mk_unit_pack {
     u_value:> X;
     u_desc: list (unit_of u_value)
@@ -255,7 +253,6 @@ Section s.
      contains, among other things, the arity of symbols)
      *)
 
-  #[universes(template)]
   Inductive T: Type :=
   | sum: idx -> mset T -> T
   | prd: idx -> nelist T -> T