Several bug-fixes:

 - URIs shortened
 - Assumption did not lift the hypothesis ==> the unification always failed

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index d2f168ce9ac36478bc51de9c1a51d0e208a83ea8..53a1347ada7a401b11d51aff06a39d46538394d0 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -70,13 +70,13 @@ let symmetry_tac ~status:(proof, goal) =
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
      match (R.whd context ty) with 
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) ->
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
          PrimitiveTactics.apply_tac ~status:(proof,goal)
-          ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/sym_eq.con", []))
+          ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
 
       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
          PrimitiveTactics.apply_tac ~status:(proof,goal)
-          ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con", []))
+          ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
 
       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
 ;;
@@ -90,18 +90,20 @@ let transitivity_tac ~term ~status:((proof, goal) as status) =
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
      match (R.whd context ty) with 
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) ->
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
          Tl.thens
           ~start:(PrimitiveTactics.apply_tac
-            ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", [])))
-          ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
+            ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
+          ~continuations:
+            [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
           ~status
 
       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
          Tl.thens 
           ~start:(PrimitiveTactics.apply_tac
-            ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", [])))
-          ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
+            ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
+          ~continuations:
+            [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
           ~status
 
       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
@@ -114,6 +116,7 @@ let assumption_tac ~status:((proof,goal) as status) =
   let module C = Cic in
   let module R = CicReduction in
   let module T = CicTypeChecker in
+  let module S = CicSubstitution in
    let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
      let rec find n = function 
@@ -124,8 +127,11 @@ let assumption_tac ~status:((proof,goal) as status) =
            | None -> prerr_endline("#### None")
          );
 *)         (match hd with
-             (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n
-           | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n 
+             (Some (_, C.Decl t)) when
+               (R.are_convertible context (S.lift n t) ty) -> n
+           | (Some (_, C.Def t)) when
+               (R.are_convertible context
+                (T.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
            | _ -> find (n+1) tl
          )
       | [] -> raise (ProofEngineTypes.Fail "No such assumption")