fixed bug in coercion application, input/output swapped in unification

[helm.git] / helm / software / components / ng_tactics / nInversion.ml

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index a93e7f5131ad6d23bbda4735e16967ab1af4cbf3..f70999315558341ec36d9a5c4b2971c7eb8e0bb8 100644 (file)
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -130,7 +130,8 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
 
  let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
                          (baseuri ^ name ^ ".def",
-                           0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in 
+                           0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
+                           (CicNotationPt.Implicit (`Tagged "inv")),`Regular)) in 
  let uri,height,nmenv,nsubst,nobj = theorem in
  let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
  let status = status#set_obj theorem in