diff options
| author | Pierre-Marie Pédrot | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 /ltac | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d8c9339121..142f061b5a 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2100,11 +2100,13 @@ let interp_redexp env sigma r = let _ = let eval ty env sigma lfun arg = + let ty = EConstr.Unsafe.to_constr ty in let ist = { lfun = lfun; extra = TacStore.empty; } in if Genarg.has_type arg (glbwit wit_tactic) then let tac = Genarg.out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - Pfedit.refine_by_tactic env sigma ty tac + let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + (EConstr.of_constr c, sigma) else failwith "not a tactic" in |