parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_unification / cicMetaSubst.ml

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 91368cde95549c1fdc096561720ebee7e90dc442..8db1cf82f31c3759a33cb4f5b14e850d2a5c6c22 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -300,14 +300,11 @@ match subst with
 let ppterm ~metasenv subst term =
  CicPp.ppterm ~metasenv (apply_subst subst term)
 
-let ppterm_in_name_context ~metasenv subst term name_context =
- CicPp.pp ~metasenv (apply_subst subst term) name_context
-
 let ppterm_in_context ~metasenv subst term context =
  let name_context =
   List.map (function None -> None | Some (n,_) -> Some n) context
  in
-  ppterm_in_name_context ~metasenv subst term name_context
+  CicPp.pp ~metasenv (apply_subst subst term) name_context
 
 let ppterm_in_context_ref = ref ppterm_in_context
 let set_ppterm_in_context f =
@@ -323,28 +320,29 @@ let ppterm_in_context ~metasenv subst term context =
 let ppcontext' ~metasenv ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
-   (fun context_entry (i,name_context) ->
+   (fun context_entry (i,context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context ~metasenv subst t name_context),
-          (Some n)::name_context
+          (ppterm_in_context ~metasenv subst t context),
+          context_entry::context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_name_context ~metasenv subst ty name_context)
-          (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
+          (ppterm_in_context ~metasenv subst ty context)
+          (ppterm_in_context ~metasenv subst bo context),
+          context_entry::context
        | None ->
-          sprintf "%s_ :? _" (separate i), None::name_context
+          sprintf "%s_ :? _" (separate i), context_entry::context
     ) context ("",[])
 
 let ppsubst_unfolded ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t,ty)) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d : %s := %s" context idx
-(ppterm_in_name_context ~metasenv [] ty name_context)
-          (ppterm_in_name_context ~metasenv subst t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv subst t context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
@@ -355,9 +353,9 @@ let ppsubst ~metasenv subst =
   String.concat "\n"
     (List.map
       (fun (idx, (c, t, ty)) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
-         sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
-          (ppterm_in_name_context ~metasenv [] t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in
+         sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context)
+          (ppterm_in_context ~metasenv [] t context))
        subst)
 ;;
 
@@ -368,9 +366,9 @@ let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
-         sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_name_context ~metasenv subst t name_context))
+        let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" scontext i
+          (ppterm_in_context ~metasenv subst t context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))
@@ -627,7 +625,14 @@ let delift n subst context metasenv l t =
 
  let module S = CicSubstitution in
   let l =
-   let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+   let (_, canonical_context, _) =
+    try
+     CicUtil.lookup_meta n metasenv
+    with CicUtil.Meta_not_found _ ->
+     raise (MetaSubstFailure (lazy
+      ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+       "declared in the metasenv")))
+    in
    List.map2 (fun ct lt ->
      match (ct, lt) with
      | None, _ -> None