diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /plugins/decl_mode | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (diff) | |
Removing the need of evarmaps in constr internalization.
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b21037d25..6e53ae6a2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1456,8 +1456,7 @@ let do_instr raw_instr pts = let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env} in + let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in |