From 6fe855a9ae94552950eaa7f1d5e926ffdd463131 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Feb 2004 18:06:28 +0000 Subject: [PATCH] sort metavariables are now generated in an empty canonical context. --- helm/ocaml/cic_unification/cicMkImplicit.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 99e599ab2..fc429b381 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -28,8 +28,8 @@ let new_meta metasenv = let mk_implicit metasenv context = let newmeta = new_meta metasenv in let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, context, Cic.Sort Cic.Type ; - newmeta + 1, context, Cic.Meta (newmeta, irl); + ([ newmeta, [], Cic.Sort Cic.Type ; + newmeta + 1, context, Cic.Meta (newmeta, []); newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) @@ -63,9 +63,8 @@ let fresh_subst metasenv context uris = let mk_implicit_type metasenv context = let newmeta = new_meta metasenv in - let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, context, Cic.Sort Cic.Type ; - newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv, + ([ newmeta, [], Cic.Sort Cic.Type ; + newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, newmeta + 1) let expand_implicits metasenv context term = -- 2.39.2